COMMENT ⊗   VALID 00015 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	
C00006 00003	.BEGIN DOUBLE SPACE
C00011 00004	.BEGIN DOUBLE SPACE
C00016 00005	The first example is so simple that we shall  just type it in on-line.
C00019 00006	.NEXT PAGE
C00023 00007	Now let's run the third example. Assume that the axiomatization is on a file named
C00028 00008	.BEGIN DOUBLE SPACE
C00032 00009	II. COMMANDS TO EXAMINE THE LIST OF CLAUSES
C00035 00010	.BEGIN DOUBLE SPACE
C00038 00011	INsert		IN <id> <statements>  IN <id> DSK: <file>
C00041 00012	III. COMMANDS FOR PERFORMING RULES OF INFERENCE
C00045 00013	IV. COMMANDS FOR SUB-PROOFS AND PROOF-CHECKING.
C00050 00014	Example 5.  A simple example of  subproof generation.
C00052 00015	When the prover is unable to make new deductions which satisfy the current
C00055 ENDMK
C⊗;

Preliminary User's Manual for the Theorem Prover
.BEGIN DOUBLE SPACE

The current program is a resolution- and paramodulation-based theorem prover
with extensive facilities for on-line control.
Many of the other facilities are quite  rudimentary.
The pattern matching and subroutining aspects of the prover
will be revised significantly.

Perhaps the easiest introduction
is to follow the development of a few examples.
.END
.BEGIN VERBATIM


Example 1.
Consider the following simple problem from propositional calculus:

Given  A ⊃ B, and ¬A ⊃ B, prove B.

This problem could be presented to the prover as:

PRE_PRED: A,B;
HYPS: A⊃B;
     ¬A⊃B;
THM:  B;
      ;

Or perhaps in a less trivial vein:


Example 2.
Consider the following set of statements:

(1)	(∀x∀y){P(x,y) ∧ P(y z) ⊃ G(x,z)}

(2)	(∀y∃x){P(x,y)}

We might interpret these statements as claiming
	"For all x and y, if x is the parent of y and y is the parent
        of z, then x is the grandparent of z,"
and
	"Everyone has a parent."
.END;


Given these statements as hypotheses we might wish to know if there were individuals, x and
 y such that x is the grandparent of y. We could pose that question as the statement:

.BEGIN VERBATIM

(3)	 (∃x∃y){G(x,y)}

.END;


It is  clear that (3) does indeed follow from (1) and (2). How do we  formulate the problem for the 
theorem prover? 

Here is one axiomatization:

.BEGIN VERBATIM
PRE_PRED: P,G; 
VAR:x,y,z;


G1: ∀(x,y)(P(x,y) ∧ P(y,z) ⊃ G(x,z)); 
G2: ∀y∃x P(x,y); 
THM: ∃(x,y)G(x,y); 
;
.END;


.BEGIN DOUBLE SPACE
Some of the conventions displayed in the examples are:

(1) the predicate letters and function symbols must be declared
according to their type.  For example infix and prefix operators are
declared  by INF_OP and PRE_OP respectively. Constants are considered to be
prefix operators of zero arguments. Similarly infix and prefix predicate
symbols must be declared as INF_PRED and PRE_PRED respectively. 
Propositional letters  should be declared to be prefix predicate symbols.
(2) variables must be declared;actually the effect of the variable declaration
is to declare the identifier as a variable prefix.  The set of variables is
automatically augmented to include 9 additional `subscripted' variants of each
declared variable.
For example,if x any y are declared variables then  x1,x2,..,x9,y1,y2...,y9 .
are also  variables and need not be declared.
(3) each statement must be terminated with a semi-colon;
(4) statements or sets of statements may be labeled.
These labels can by used to refer to clauses in the on-line editor.  If a statement is labeled, 
THM, then the negation of that statement is formed and is used in the list of input statements.
The identifier used to name the theorem may be changed by modifying the LISP value
of the atom THEOREMNAME.(Thus the default value of THEOREMNAME is THM.)
(5) adjacent like quantifiers may  combined.
(6) the whole set of declarations and input statements must be delimited by a semicolon. 

A complete description of the syntax and semantics of the input format 
is given in the Appendix.
.END 

.NEXT PAGE

Example 3.

In an investigation of axiomatizations of elementary group theory the following statements
arose:

.BEGIN VERBATIM

(1)	x*x = y*y
(2)	x*(y*y) = x
(3)	x*(y*z) = z*(y*x)
(4)	x*(x*y)  = y
(5)	(x*z)*(y*z) = x*y

.END;

Question: Does (5) follow from (1)-(4)?

The answer is "yes" but it is not immediately obvious.  It is more difficult 
to establish than Example 2.
Notice that this example is a pure equality formulation, (i.e., equality is the only
predicate so that all formulas are in fact equations).
This example could be presented to the prover as:

.BEGIN VERBATIM

INF_OP: *;
INF_PRED: =;EQUALITY:=;
VAR: x,y,z;
AXIOMS: x*x = y*y;
	x*(y*y) = x;
	x*(y*z) = z*(y*x);
	x*(x*y) = y;
THM:(x*z)*(y*z) = x*y;
;
.END;

In this example, the name AXIOMS, refers the first four statements.

Before presenting a more complicated example, we shall describe how to use the prover
on these first Examples.





.NEXT PAGE

.BEGIN DOUBLE SPACE
Once the input file has been prepared you are ready to used the theorem prover.
The command: RUN PROVER [P,JRA] , will select the current version of the program.
The appearence of an asterisk (*) signifies that the program is ready.
If you wish the program to make an initial selection of strategies  for your problem
then type: (PROVE DSK: filename). The exact strategies which are chosen are described in
Section VIII.
If you would rather  select you own strategies then type: (TRY DSK: filename).
You will then be asked to describe your choice and editing strategies.
See Section VIII for a complete description of strategy selection.

If the (translations of) the set of input statements are found to be inconsistent,
then the sequence of deductions which exhibits that
inconsistency is displayed on the console.  This refutation and the set of strategies
which were employed are also saved on a disk file . The name of the file 
is created from the name of the input file.
Thus, for example, (PROVE DSK: FOO) and (PROVE DSK: (FOO.A)) would create an output
file named N1FOO.PRF. If the  input initially comes for the console using (PROVE) or (TRY), 
then the output file is given the  name, N1PRF.PRF.
It is also possible that the prover terminate without finding a refutation.
This could occur either because the selected strategies do not form a complete set
or because the initial set is not inconsistent. In either case the program types
 NO-PROOF-FOUND and enters the clause editor to wait for commands from the user.

.END;

.NEXT PAGE


The first example is so simple that we shall  just type it in on-line.
The output will then be found on the file N1PRF.PRF.
Material preceeded by | is commentary; statements typed by the user are
preceeded by *.

.BEGIN VERBATIM
*RU PROVER [P,JRA]		|retrieve the prover.

*(PROVE)			|The prover is to pick strategies.
*PRE_PRED:A,B;
PRE_PRED:A,B;			|Declaration is echoed by prover.
*HYPS: A⊃B;¬A⊃B;
HYPS				|The  statements are echoed.
A⊃B;
¬A⊃B;
*THM:B;				|We wish to prove B.
THM
B;
*;				|This final semicolon signals the end
				|of the input.
HERE-ARE-THE-CLAUSES:		|Here are the translations of the 
				|input statements.
1 A⊃B;
2 B∨A;
3 ¬B;				|Notice that the statement of the
				|theorem(THM) has been negated.
4 A;				|The first deduction.
5 ¬A;				|Another deduction.
COUNT 3
LEVEL 1				|These are statistics printed by the 
ELAPSED-TIME 134		|prover.
6 B;
COUNT 5
LEVEL 2				|The end of level-2 deductions.
ELAPSED-TIME 288
.GROUP
				|A proof  has been found.
NIL 1 6				|Here's a proof-tree:
1 B; 3 4			|  6    5
3 A; 5 6			|   \  /
4 A⊃B; HYPS			|    3    4
5 B∨A; HYPS			|     \  /
6 ¬B; THM			|       1    6
*				|        \  /
				|         NIL
.APART
.END
Notes:
.NARROW 8
1. Though all statements are stored internally in conjunctive normal form,
an attempt is made to improve the readibility on output. Clauses are translated
for output as follows:

a)clauses containing only positive literals appear as a disjunction.

b)clauses containing only negative leterals appear as the negation of
a conjunction.

c)mixed clauses, containing positive and negative literals appear in the
form of an implication.

.WIDEN
.NEXT PAGE
Now let's try running the second example.  Assume that a disk file, EX1, has been prepared
containing the axiomatization. What follows is a running commentary on what should 
occur.

.BEGIN VERBATIM

*RUN PROVER [P,JRA]		|retrieve the current prover.

*(PROVE DSK: EX1)		|Request that the program pick the
				|strategies while running EX1.
PRE_PRED: P,G;			|The program is accepting the axioms.
VAR: x,y,z;
G1:
∀(x,y)(P(x,y) ∧ P(y,z)) ⊃ G(x,z));
G2:
∀y∃x P(x,y);
THM:
∃(x,y)G(x,y);

HERE-ARE-THE-CLAUSES:		|What follows are the translations 
				|of the input into clause-form, with
1 P(x,z)∧P(y,z) ⊃ G(x,y)    	|the redundant statements removed.
2 P(G21(x),x)  			|G21 is a generated Skolem function.
3 ¬G(x,y)			|The translation of the negation of 
				|the theorem.

4 ¬(P(z,x)∧P(x,y)) 		|A deduction which has been added to 
				|the list of clauses.
COUNT = 1			|There was only one resolvent formed
LEVEL = 1			|on level one.
ELAPSED-TIME = 333		|The execution time in milliseconds.

.GROUP
5 ¬P(x,y);

COUNT = 3
LEVEL = 2			|Three resolvents have been formed by
ELAPSED-TIME = 500		|the end of level 2. (Two have been 
				|retained.)
NIL 1 4				|A contradiction. These next six 
1 -P(x,y) 3 4			|lines are the refutation. I.e.:
3 ¬(P(z,x)∧P(x,y)) 5 6	 	|  6    5
4 P(G21(x),x) G2	     	|   \  /
5 P(x,z)∧P(y,z) ⊃ G(x,y) G1	|     3     4
6 ¬G(x,y) THM			|       \  /
				|         1    4
				|          \  /
				|            NIL


.APART
.END;
.GROUP
Notes: 
.NARROW 8;

1. The labeling of the input is reflected in the description of the
refutation tree. That is, P(G21(x),x) resulted from the translation of G2;
¬G(x,y) came from the negation of the theorem.

2. A copy of the refutation tree, relevant statistics, and  a description of the
actual strategies used, now appears on a file named N1EX1.PRF.

.WIDEN
.APART
.NEXT PAGE

Now let's run the third example. Assume that the axiomatization is on a file named
 EX2.

.BEGIN VERBATIM 

*RUN PROVER [P,JRA]

*(PROVE DSK: EX2)		|Again, let the program
				|pick the strategies.
INF_OP: *;
INF_PRED: =;
EQUALITY: =;
VAR:x,y,z;
AXIOMS:
x*x=y*y;
x*(y*y)=x;
x*(y*z)=z*(y*x);
x*(x*y)=y;
THM:
(x*z)*(y*z)=x*y;

HERE-ARE-THE-CLAUSES:

1 x*x=y*y 
2 x*(y*y)=x
3 x*(y*z)=z*(y*x)
4 x*(x*y)=y
¬(THM1*THM3)*(THM2*THM3)=THM1*THM2
				|Again, THMn's are generated
				|Skolem constants.

NIL 1 2				|An immediate contradiction
1 x=x;			     |We know E is reflexive
2 ¬THM1*THM2=THM1*THM2;	 3 4 |moderate mystery.
3 x*(y*z)=z*(y*x); AXIOMS
4 ¬(THM1*THM3)*(THM1*THM2)=THM1*THM2; THM
.END;

Notes:



1. The `refutation' is a bit mysterious.  A more sympathetic proof recovery
mechanism is contemplated, but perhaps some of the current mystery can be dispelled.

A `natural' proof might be:

.BEGIN VERBATIM
	1.  (x*z)*(y*z) = z*(y*(x*z))  replacement using (3)
	2.  z*(y*(x*z)) = z*(z*(x*y))  replacement using (3)
	3.  z*(z*(x*y)) = x*y          replacement using (4)
.END;

.BEGIN DOUBLE SPACE
The above proof is indeed a translation of the machine proof.  Besides replacement,
the prover also has a special rule of simplification. Whenever an equality
formulation is presented to the prover, a list ,SL,is made consisting
 of all the equalities which occur in the input.
In the current example, SL would consist of everything but the negation of the 
theorem. Let  t1 = t2 be a member of SL. Whenever a deduction is formed  (but before
it has been added to the memory of the prover) we attempt to match t1 against terms
occurring in the deduction. If matches can be made we replace those terms with the
appropriate instance of t2. It is this simplified deduction which is presented to the
editing strategies of the prover.

.END;



.GROUP

Thus the refutation really is:
.BEGIN VERBATIM

¬(THM1*THM3)*(THM2*THM3)=THM1*THM2  THEOREM
	\
	  \
	    \  x*(y*z)=z*(y*x) AXIOMS
	      \      /
		\  /
¬THM3*(THM2*(THM1*THM3))=THM1*THM2  by replacement 
		\        
	  	  \
		    \ x*(y*z)=z*(y*x)  AXIOMS
		      \       /
			\   /
¬THM3*(THM3*(THM1*THM2))=THM1*THM2  by simplification 
		\	
		  \
		    \ x*(x*y)=y  AXIOMS
		      \       /
			\   /
         ¬THM1*THM2=THM1*THM2  by simplification 
 	       \ 
		 \
		   \          x=x
		     \        /
		       \    /
			NIL
				by resolution
.END;
.APART


.NEXT PAGE

.BEGIN DOUBLE SPACE
Most applications of the prover lie in that gray area between a quick proof and the occurrence of 
NO-PROOF.  That is, an application of the prover usually generates a large number
of deductions before either a proof is found or no more deductions can be made
under the current strategy settings.
It is this area which can be profitably explored using interactive commands.
If the user sees a deduction which  should lead to the desired  refutation
he is able to guide the program to the explicit contradiction.  If he sees
a deduction which he feels is interesting, he can explore its consequences in the
set of statements.  If he feels that the strategy settings are ill-chosen
then he can abort the current proof-search and pick new strategies.  The next
sections give detailed descriptions of the current on-line commands.

First, the on-line editor is entered by striking the space bar.

.END;
I. GENERAL BOOKEEPING COMMANDS.

CHange		CH;
.NARROW 16;
It is  frequently desireable to change some of the strategies while a proof attempt is in progress.
CHange describes what choice and editing strategies are currently active and 
asks which are to be changed.
.WIDEN;

CUrrent		CU;
.NARROW 16;
This command simply lists the current strategy settings.
.WIDEN;

DSkout		DS <filename>;
.NARROW 16;
This command diverts future output to specified disk file. 
.WIDEN;

EVal	 	EV;
.NARROW 16;
This command is  mostly a debugging aid and is included for completeness.  The casual users should not have to resort
to its use.  EVal enters a READ-EVAL-PRINT. To return to the editor, type @END.
.WIDEN;

HAlt		HA;
.NARROW 16;
HAlt stops the prover is such a state that if the current core image is saved, it can
be continued.  To  resume execution of such a core image, type RUN  DSK: name.  When the
asterisk appears you are in the on-line editor. Then type TErminate.
.WIDEN;

End Of file	EO;
.NARROW 16;
EOf is used to terminate the DSkout command.

.WIDEN;
HElp		HE;
.NARROW 16;
This command will type a list of the available editing commands along with an abbreviated description of their action.
.WIDEN;

TErminate 	TE;
.NARROW 16;
This command is used to terminate the use of the on-line editor and return to the prover.
.WIDEN;






.NEXT PAGE

II. COMMANDS TO EXAMINE THE LIST OF CLAUSES
.BEGIN DOUBLE SPACE

Each  clause which has been retained by the prover -- initial clauses or 
deduction -- is given a number, the first axiom, the
number 1., etc.. These numbers are permanently assigned, even though certain
actions of the prover may delete  clauses from active status in which case they are
not used in making  any future deductions.
Clauses which have been so deleted are displayed as *DE*.  When the editor is entered,
a hypothetical pointer is initialized to the first clause.  This first  set of commands
allow the used to manipulate the set of clauses using the associated numbers.

.END;

FLoat UP	FU; or FL UP;
.NARROW 16 ;
Moves the pointer up through the list of clauses.  The motion is stopped
either by striking a key or by reaching the upper extreme of the
list. FLoat UP may also be apbbreviated as FU.
.WIDEN;

FLoat DOwn	FD; or FL DO;
.NARROW 16;
The counterpart of FLoat UP. FLoat Down may also be abbreviated 
as FD.
.WIDEN;

UP		UP n;
.NARROW 16;
UP is to be followed by an integer, n.  The effect of this command
is to move the pointer up n clauses from its current  setting. As the pointer
is moved, the interviening clauses are printed.
If n = 0, then the pointer is immediately moved to the beginning of the 
clause list.  As with the FLoat commands,striking a key will stop the pointer.
.WIDEN;

DOwn		DO n;
.NARROW 16;
The counterpart of UP. DOwn 0 moves the pointer to the end of
the list.
.WIDEN;

GO		GO n;
.NARROW 16;
GO is to be followed by an integer designating a clauses.  The pointer goes  
immediately to the designated clause.
.WIDEN;

.NEXT PAGE

.BEGIN DOUBLE SPACE
Though these commands  have proved quite useful, experience  has shown that more
global manipulation of the clauses is needed. Therefore we have commands for
assigning names to subsets of the clause list, and commands for manipulating these sets.
Just as each element of the primary list of clauses is assigned a unique positive integer,
so is each element of each named subset.  For example to refer to the second element of the
set  named FOO, use FOO[2]; to refer to the second and third elements, use FOO[2,3].
Certain commands, like REsolve or PAramodualte create new names, like RES1,RES2, etc.
or PAR1, PAR2. These created names are local to that call on the on-line editor.
Names which were initiated by the user using the SEt command are global.

The following BNF equations will be used in the sequel:
 
.END;
.BEGIN VERBATIM;
<clauses> ::= {<c>,}*<c>

<c>	  ::= <number>|<id>{[{<number>,}*<number>]}*

	  ::= @<statment>|FIND[<id>;<pattern>]

.END;

ANcestry	AN <clauses>;
.NARROW 16;
The ancestry command is used to display the derivation tree of the specified clauses.
.WIDEN
CLear		CL <id>;	
.NARROW 16;
CLear takes a name as argument. This command only removes the
name from the symbol table; it does not affect the clauses attached to the
name.
.WIDEN;

Delete		DE <clauses>;
.NARROW 16;
The designated clauses are deleted from the memory of the prover. Attempts to display
 such clauses will print *DE*.  Other attempts to use deleted clauses in editing commands
will  invoke an error message.
.WIDEN;

DIsplay		DI <clauses>;
.NARROW 16;
This command displays all the elements of <clauses>;_
.WIDEN;



INsert		IN <id> <statements>;  IN <id> DSK: <file>;
.NARROW 16;
This command is used to enter new clauses into the  clause editor.
The first argument to INsert is a <name>. What follows is a set of clauses, or a file designator.
If the clauses are typed they must conform to the standard input format; if a file
designator is given, the specified file must be in the correct format. IN is a special
case of the SEt command.
.WIDEN;

SAve		SA <clauses>;
.NARROW 16;
Most of the results of the  on-line commands: deductions, insertions, substitutions,etc,
are local to the clause editor. To include any of these resulting clauses in the memory of the prover
use the Save command.
.WIDEN;


SEt		SE <id> <clauses>;
.NARROW 16;
SEt <id> <clauses>; has the effect of assigning
to <id>, the sequence of clauses selected by the <clauses>.
Within a particular proof attempt, the names selected by the user are retained.
.WIDEN;

SUbstitute	SU <term>; FOR <term>; IN <clauses>;
.NARROW 16;
The effect of the SUbstitute command is to substitute the first <term> for
every occurrence of the second <term> in copies of all of the designated <clauses>.
Notice that the original <clauses> are kept intact. The modified  <clauses>
are added to the list named ASSERT.
.WIDEN

.NEXT PAGE
.BEGIN DOUBLE SPACE

The commands listed above give us a reasonably powerful set of instructions for
manipulating the clause list. Clearly, before we can really begin to guide the prover
we must be able to perform the rules of inference on-line. The next  set of commands
begins to do this.


.END;



III. COMMANDS FOR PERFORMING RULES OF INFERENCE



PAramodulate		PA <clauses>; <clauses>;
.NARROW 16;
This command handles equality replacements.
All equality literals of the form t1=t2, are used in equality replacements in the following manner:
let s be any term, not a variable, which occurs in some literal in one of the clauses.
If s occurs no deeper than PDEPTH (see the appendix for PDEPTH) and there is a substitution
 unifying s and t1, then the occurrence of t1 is replaced by the appropriate instantiation
of t2.
.WIDEN;

REsolve			RE <clauses>;<clauses>;
.NARROW 16;
This command takes a pair of <clauses> as arguments.  The resolvents of these
two sets are formed, a unique name is generated and the resolvents are assigned to that
new name.  The generated names are presently of the form RESn, for some integer,n.
.WIDEN;

SImplify		SImplify <clauses>; BY <clauses>;
.NARROW 16;
This command is similar to the PA command.  Here the second set of clauses is to be a
list of equality units, again of the form t1=t2. Terms occuring in the first set of clauses
which unify with elements, t1, are replaced by instances of t2.  DDEPTH determines the
depth to which the match is attempted.
.WIDEN;

Example 4.  A simple example of the use of the rules of inference.

Assume that = is the equality predicate and that we have just struck a key on the
console.

.BEGIN VERBATIM


*DI 1,2,3;			|Display the first three clauses
1 x≤y ⊃ x/y=0
2 ¬1/(a/b)=0
3 0≤x

*PA 1; 2;			|Use replacement on 1 and 2.
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME: PAR1	|PAR1 is a created name.

1 1≤a/b ⊃ 1=0

*PA 2; 3;			|Try to use the replacement rule
NO-PARAMODULANTS		|on clauses 2, and 3.

*RE 1; 3;
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME:RES1	|RES1 is another created
				|name.
1 0/x=0

*PA RES1; RES1;			|Created names are legal.
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME:PAR2	|PAR2 is a new name.

1 0=0				|True.

*SA PAR1[1];			|Add 1≤a/b ⊃ 1=0 to the memory
				|of the prover;

.END;

.NEXT PAGE


IV. COMMANDS FOR SUB-PROOFS AND PROOF-CHECKING.

.BEGIN DOUBLE SPACE
Though the commands, REsolve and PAramodulate, are useful for fine control of the
prover, is is often useful to demand larger inference steps. That is, using some of the
existing clauses in memory, with perhaps some additional assumptions, we wish the
prover to attempt to establish the validity of a  first order formula. While this
subproof is  under investigation the state of the main proof should be preserved.
The commands in this section are used to initiate and control such subproofs.

.END;


ABort		AB ; or AB <clauses>;

.NARROW 16;
This command is used to manually abort a proof attempt, returning to the previous
level.  If <clauses> is present, then the selected clauses are returned and assigned
to a created name.
.WIDEN;


USing		US <clauses>; or US DSK: <file>;
.NARROW 16;
The selected clauses are designated to be used in the forthcoming
subproof.
.WIDEN;

PRove		PR <statement>; or PR DSK: <file>;
.NARROW 16;
The <statement> is translated and will be attached to the name LEMMA. The negation 
of the statement is also formed and will be used in the subproof. Thus both the positive and negative 
tanslates are formed.  The positive translate is maintained for the convenience of the
user since after the lemma has been established  it  should be available for further 
deductions.  Within the subproof the negation of the <statement> will appear under the local
name, THMS.
.WIDEN;

These last two commands,--USing, and PRove -- are used to initialize the call
on the prover; USing may be omitted. There are two  commands to
commence the subproof.

EXecute		EX;
.NARROW 16;
EXecute begins the subproof using a computed set of stategies.
.WIDEN;

TRy		TR;
.NARROW 16;
TRy first enters the strategy selection dialog, then begins the subproof with the chosen strategies.
.WIDEN;

In both cases the strategies of the subproof are completely local.  They in no way
affect the strategies in the parent proof. If a key is struck while in the subproof
the editor is entered and can manipulate the local clauselist or initiate another
subproof. The TErminate command will comtinue the subproof, the ABort command will
return to the previous level.


.NEXT PAGE

Example 5.  A simple example of  subproof generation.

Suppose that we have struck a key during a proof-search.
.BEGIN VERBATIM

*AN 10;				|Display the ancestry of 
P(A) 1 2			|clause no. 10.
1 P(A) ∨ P(B)  AX1
2 ¬P(B)	     HYP1

*USING 10, @P(A) ⊃ P(B); ;	|Setup the assumptions for the
				|lemma.
				|Use clause no. 10 in the attempt

*PROVE @P(B);;

*EX;				|This initiates the subproof.

NIL 1 2
1 P(A) DEDUCT			|Clause 10 becomes an "axiom"
2 ¬P(A)	3 4			|with the subproof.
3 P(A)⊃P(B)  INSERT 
4 ¬P(B) THM	 		|The negation of the lemma

PROOF-FOUND-FOR-LEMMA
				|We are now back in the  editor
*DI 10;				|Display clause no. 10.
P(A)

*DI LEMMA;			|The translate of the statement 
P(B)				|to be PROVEed.

*USING LEMMA;

*PROVE @∃(x)P(x);;		|LEMMA now becomes the translate
*EX;				|this clause.
NIL 1 2
1 P(B) AX1
2 ¬P(X1) THM

PROOF-FOUND-FOR-LEMMA

*DI LEMMA;			|ED1 is a ubiquitous Skolem 
P(ED1)				|constant.
.END;

.NEXT PAGE


V. COMMANDS USEFUL WHEN NO PROOF IS FOUND

.BEGIN DOUBLE SPACE

When the prover is unable to make new deductions which satisfy the current
strategies it will report that no refutation can be found, and will enter
the on-line editor. At this time  the user can examine the list of clauses,
perform rules of inference, initiate sub-proofs,
save any or all of the current deductions
and begin a the proof search again, perhaps with new strategies.
The user can also force a proof attempt to be abandoned by typing AB;.  This
has exactly the same effect as if the prover could make no new deductions.

.END;

ABandon		AB;

.NARROW 16
AB, typed in this context (not in a subproof) terminates the main proof attempt,
enters the on-line editor, and waits for commands.
.WIDEN

TErminate	TE <clauses>; or TE;

.NARROW 16
If <clauses> are present then they are added to the list of clauses named THMS.
The list, AXIOMS, HYPS, and THMS are preserved and a new proof attempt is begun.
If the initial attempt was through PROVE then the user is asked if he still wants
automatic strategy selection.  If the initial attempt was through TRY or the
user does not wish automatic selection, then a dialogue is begun describing the
current strategies and asking if changes are desired.
Then a new proof search is begun.
.WIDEN

.BEGIN DOUBLE SPACE

This use of AB and TE is useful for feeding `interesting' deductions back into a
proof search without having to restart the whole process.  The derivation tree
of any such saved derived clause is maintained for the proof recovery mechanisms
but such clauses appear to be `input' clauses to the rules of inference.

.END;